($\lambda$$T$,$l$,$x$,$P$,$z$. $y$ = succ($x$) in $l$$\Rightarrow$ $P$($y$)) $\in$ $T$:Type$\rightarrow$($T$ List)$\rightarrow$$T$$\rightarrow$($T$$\rightarrow$Prop)$\rightarrow\downarrow$True$\rightarrow$Prop